A:Type, B:(AType).
(a, b:A. Dec(a = b))  (a:A, u, v:B(a). Dec(u = v))  (x, y:(a:AB(a)). Dec(x = y)) 

latex

Definitions	P  Q, x(s), Prop, x:A. B(x), t  T, Dec(P), P  Q, A, {T}, False, 2of(t), 1of(t), x. t(x)
Lemmas	pi1 wf, pi2 wf, not wf, decidable wf